
(* 

 ------------ INIT
  G, A |- A

*)

let INIT = ASSUME

(*
  G |- A    G |- B
 ------------------ ANDR
    G |- A /\ B
*)

let ANDR = CONJ


(* 
     G, A |- C
------------------ ANDL1
  G, A /\ B |- C
*) 

let ANDL1 a b thm =
  (* A /\ B ==> A *)
  let ab = mk_conj(a, b) in
  let aba = DISCH ab (CONJUNCT1 (ASSUME ab)) in
  (* G |- A ==> C *)
  let ac = DISCH a thm in
  (* G |- A /\ B ==> C *)
  let abc = IMP_TRANS aba ac in
    UNDISCH abc

(* 
     G, B |- C
------------------ ANDL1
  G, A /\ B |- C
*) 

let ANDL2 a b thm =
  (* A /\ B ==> A *)
  let ab = mk_conj(a, b) in
  let aba = DISCH ab (CONJUNCT2 (ASSUME ab)) in
  (* G |- A ==> C *)
  let ac = DISCH b thm in
  (* G |- A /\ B ==> C *)
  let abc = IMP_TRANS aba ac in
    UNDISCH abc
